↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(Y, Z), W) → U7_aga(X, Y, Z, W, delete_in_aaa(X, Z, W))
delete_in_aaa(X, .(X, Y), Y) → delete_out_aaa(X, .(X, Y), Y)
delete_in_aaa(X, .(Y, Z), W) → U7_aaa(X, Y, Z, W, delete_in_aaa(X, Z, W))
U7_aaa(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aaa(X, .(Y, Z), W)
U7_aga(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aga(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_aa(Z, V))
perm_in_aa([], []) → perm_out_aa([], [])
perm_in_aa(.(X, .(Y, [])), .(U, .(V, []))) → U5_aa(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
U5_aa(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_aa(X, Y, U, V, perm_in_aa(Z, V))
U6_aa(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_aa(.(X, .(Y, [])), .(U, .(V, [])))
U6_ag(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_aa(X, Y))
le_in_aa(s(X), s(Y)) → U8_aa(X, Y, le_in_aa(X, Y))
le_in_aa(0, s(X)) → le_out_aa(0, s(X))
le_in_aa(0, 0) → le_out_aa(0, 0)
U8_aa(X, Y, le_out_aa(X, Y)) → le_out_aa(s(X), s(Y))
U3_g(X, Y, Z, le_out_aa(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PrologToPiTRSProof
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(Y, Z), W) → U7_aga(X, Y, Z, W, delete_in_aaa(X, Z, W))
delete_in_aaa(X, .(X, Y), Y) → delete_out_aaa(X, .(X, Y), Y)
delete_in_aaa(X, .(Y, Z), W) → U7_aaa(X, Y, Z, W, delete_in_aaa(X, Z, W))
U7_aaa(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aaa(X, .(Y, Z), W)
U7_aga(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aga(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_aa(Z, V))
perm_in_aa([], []) → perm_out_aa([], [])
perm_in_aa(.(X, .(Y, [])), .(U, .(V, []))) → U5_aa(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
U5_aa(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_aa(X, Y, U, V, perm_in_aa(Z, V))
U6_aa(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_aa(.(X, .(Y, [])), .(U, .(V, [])))
U6_ag(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_aa(X, Y))
le_in_aa(s(X), s(Y)) → U8_aa(X, Y, le_in_aa(X, Y))
le_in_aa(0, s(X)) → le_out_aa(0, s(X))
le_in_aa(0, 0) → le_out_aa(0, 0)
U8_aa(X, Y, le_out_aa(X, Y)) → le_out_aa(s(X), s(Y))
U3_g(X, Y, Z, le_out_aa(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
SLOWSORT_IN_AG(X, Y) → U1_AG(X, Y, perm_in_ag(X, Y))
SLOWSORT_IN_AG(X, Y) → PERM_IN_AG(X, Y)
PERM_IN_AG(.(X, .(Y, [])), .(U, .(V, []))) → U5_AG(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
PERM_IN_AG(.(X, .(Y, [])), .(U, .(V, []))) → DELETE_IN_AGA(U, .(X, Y), Z)
DELETE_IN_AGA(X, .(Y, Z), W) → U7_AGA(X, Y, Z, W, delete_in_aaa(X, Z, W))
DELETE_IN_AGA(X, .(Y, Z), W) → DELETE_IN_AAA(X, Z, W)
DELETE_IN_AAA(X, .(Y, Z), W) → U7_AAA(X, Y, Z, W, delete_in_aaa(X, Z, W))
DELETE_IN_AAA(X, .(Y, Z), W) → DELETE_IN_AAA(X, Z, W)
U5_AG(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_AG(X, Y, U, V, perm_in_aa(Z, V))
U5_AG(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → PERM_IN_AA(Z, V)
PERM_IN_AA(.(X, .(Y, [])), .(U, .(V, []))) → U5_AA(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
PERM_IN_AA(.(X, .(Y, [])), .(U, .(V, []))) → DELETE_IN_AGA(U, .(X, Y), Z)
U5_AA(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_AA(X, Y, U, V, perm_in_aa(Z, V))
U5_AA(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → PERM_IN_AA(Z, V)
U1_AG(X, Y, perm_out_ag(X, Y)) → U2_AG(X, Y, sorted_in_g(Y))
U1_AG(X, Y, perm_out_ag(X, Y)) → SORTED_IN_G(Y)
SORTED_IN_G(.(X, .(Y, Z))) → U3_G(X, Y, Z, le_in_aa(X, Y))
SORTED_IN_G(.(X, .(Y, Z))) → LE_IN_AA(X, Y)
LE_IN_AA(s(X), s(Y)) → U8_AA(X, Y, le_in_aa(X, Y))
LE_IN_AA(s(X), s(Y)) → LE_IN_AA(X, Y)
U3_G(X, Y, Z, le_out_aa(X, Y)) → U4_G(X, Y, Z, sorted_in_g(.(Y, Z)))
U3_G(X, Y, Z, le_out_aa(X, Y)) → SORTED_IN_G(.(Y, Z))
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(Y, Z), W) → U7_aga(X, Y, Z, W, delete_in_aaa(X, Z, W))
delete_in_aaa(X, .(X, Y), Y) → delete_out_aaa(X, .(X, Y), Y)
delete_in_aaa(X, .(Y, Z), W) → U7_aaa(X, Y, Z, W, delete_in_aaa(X, Z, W))
U7_aaa(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aaa(X, .(Y, Z), W)
U7_aga(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aga(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_aa(Z, V))
perm_in_aa([], []) → perm_out_aa([], [])
perm_in_aa(.(X, .(Y, [])), .(U, .(V, []))) → U5_aa(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
U5_aa(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_aa(X, Y, U, V, perm_in_aa(Z, V))
U6_aa(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_aa(.(X, .(Y, [])), .(U, .(V, [])))
U6_ag(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_aa(X, Y))
le_in_aa(s(X), s(Y)) → U8_aa(X, Y, le_in_aa(X, Y))
le_in_aa(0, s(X)) → le_out_aa(0, s(X))
le_in_aa(0, 0) → le_out_aa(0, 0)
U8_aa(X, Y, le_out_aa(X, Y)) → le_out_aa(s(X), s(Y))
U3_g(X, Y, Z, le_out_aa(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PrologToPiTRSProof
SLOWSORT_IN_AG(X, Y) → U1_AG(X, Y, perm_in_ag(X, Y))
SLOWSORT_IN_AG(X, Y) → PERM_IN_AG(X, Y)
PERM_IN_AG(.(X, .(Y, [])), .(U, .(V, []))) → U5_AG(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
PERM_IN_AG(.(X, .(Y, [])), .(U, .(V, []))) → DELETE_IN_AGA(U, .(X, Y), Z)
DELETE_IN_AGA(X, .(Y, Z), W) → U7_AGA(X, Y, Z, W, delete_in_aaa(X, Z, W))
DELETE_IN_AGA(X, .(Y, Z), W) → DELETE_IN_AAA(X, Z, W)
DELETE_IN_AAA(X, .(Y, Z), W) → U7_AAA(X, Y, Z, W, delete_in_aaa(X, Z, W))
DELETE_IN_AAA(X, .(Y, Z), W) → DELETE_IN_AAA(X, Z, W)
U5_AG(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_AG(X, Y, U, V, perm_in_aa(Z, V))
U5_AG(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → PERM_IN_AA(Z, V)
PERM_IN_AA(.(X, .(Y, [])), .(U, .(V, []))) → U5_AA(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
PERM_IN_AA(.(X, .(Y, [])), .(U, .(V, []))) → DELETE_IN_AGA(U, .(X, Y), Z)
U5_AA(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_AA(X, Y, U, V, perm_in_aa(Z, V))
U5_AA(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → PERM_IN_AA(Z, V)
U1_AG(X, Y, perm_out_ag(X, Y)) → U2_AG(X, Y, sorted_in_g(Y))
U1_AG(X, Y, perm_out_ag(X, Y)) → SORTED_IN_G(Y)
SORTED_IN_G(.(X, .(Y, Z))) → U3_G(X, Y, Z, le_in_aa(X, Y))
SORTED_IN_G(.(X, .(Y, Z))) → LE_IN_AA(X, Y)
LE_IN_AA(s(X), s(Y)) → U8_AA(X, Y, le_in_aa(X, Y))
LE_IN_AA(s(X), s(Y)) → LE_IN_AA(X, Y)
U3_G(X, Y, Z, le_out_aa(X, Y)) → U4_G(X, Y, Z, sorted_in_g(.(Y, Z)))
U3_G(X, Y, Z, le_out_aa(X, Y)) → SORTED_IN_G(.(Y, Z))
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(Y, Z), W) → U7_aga(X, Y, Z, W, delete_in_aaa(X, Z, W))
delete_in_aaa(X, .(X, Y), Y) → delete_out_aaa(X, .(X, Y), Y)
delete_in_aaa(X, .(Y, Z), W) → U7_aaa(X, Y, Z, W, delete_in_aaa(X, Z, W))
U7_aaa(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aaa(X, .(Y, Z), W)
U7_aga(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aga(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_aa(Z, V))
perm_in_aa([], []) → perm_out_aa([], [])
perm_in_aa(.(X, .(Y, [])), .(U, .(V, []))) → U5_aa(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
U5_aa(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_aa(X, Y, U, V, perm_in_aa(Z, V))
U6_aa(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_aa(.(X, .(Y, [])), .(U, .(V, [])))
U6_ag(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_aa(X, Y))
le_in_aa(s(X), s(Y)) → U8_aa(X, Y, le_in_aa(X, Y))
le_in_aa(0, s(X)) → le_out_aa(0, s(X))
le_in_aa(0, 0) → le_out_aa(0, 0)
U8_aa(X, Y, le_out_aa(X, Y)) → le_out_aa(s(X), s(Y))
U3_g(X, Y, Z, le_out_aa(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
↳ PiDP
↳ PrologToPiTRSProof
LE_IN_AA(s(X), s(Y)) → LE_IN_AA(X, Y)
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(Y, Z), W) → U7_aga(X, Y, Z, W, delete_in_aaa(X, Z, W))
delete_in_aaa(X, .(X, Y), Y) → delete_out_aaa(X, .(X, Y), Y)
delete_in_aaa(X, .(Y, Z), W) → U7_aaa(X, Y, Z, W, delete_in_aaa(X, Z, W))
U7_aaa(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aaa(X, .(Y, Z), W)
U7_aga(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aga(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_aa(Z, V))
perm_in_aa([], []) → perm_out_aa([], [])
perm_in_aa(.(X, .(Y, [])), .(U, .(V, []))) → U5_aa(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
U5_aa(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_aa(X, Y, U, V, perm_in_aa(Z, V))
U6_aa(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_aa(.(X, .(Y, [])), .(U, .(V, [])))
U6_ag(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_aa(X, Y))
le_in_aa(s(X), s(Y)) → U8_aa(X, Y, le_in_aa(X, Y))
le_in_aa(0, s(X)) → le_out_aa(0, s(X))
le_in_aa(0, 0) → le_out_aa(0, 0)
U8_aa(X, Y, le_out_aa(X, Y)) → le_out_aa(s(X), s(Y))
U3_g(X, Y, Z, le_out_aa(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
↳ PiDP
↳ PrologToPiTRSProof
LE_IN_AA(s(X), s(Y)) → LE_IN_AA(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ NonTerminationProof
↳ PiDP
↳ PiDP
↳ PiDP
↳ PrologToPiTRSProof
LE_IN_AA → LE_IN_AA
LE_IN_AA → LE_IN_AA
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
↳ PrologToPiTRSProof
U3_G(X, Y, Z, le_out_aa(X, Y)) → SORTED_IN_G(.(Y, Z))
SORTED_IN_G(.(X, .(Y, Z))) → U3_G(X, Y, Z, le_in_aa(X, Y))
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(Y, Z), W) → U7_aga(X, Y, Z, W, delete_in_aaa(X, Z, W))
delete_in_aaa(X, .(X, Y), Y) → delete_out_aaa(X, .(X, Y), Y)
delete_in_aaa(X, .(Y, Z), W) → U7_aaa(X, Y, Z, W, delete_in_aaa(X, Z, W))
U7_aaa(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aaa(X, .(Y, Z), W)
U7_aga(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aga(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_aa(Z, V))
perm_in_aa([], []) → perm_out_aa([], [])
perm_in_aa(.(X, .(Y, [])), .(U, .(V, []))) → U5_aa(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
U5_aa(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_aa(X, Y, U, V, perm_in_aa(Z, V))
U6_aa(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_aa(.(X, .(Y, [])), .(U, .(V, [])))
U6_ag(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_aa(X, Y))
le_in_aa(s(X), s(Y)) → U8_aa(X, Y, le_in_aa(X, Y))
le_in_aa(0, s(X)) → le_out_aa(0, s(X))
le_in_aa(0, 0) → le_out_aa(0, 0)
U8_aa(X, Y, le_out_aa(X, Y)) → le_out_aa(s(X), s(Y))
U3_g(X, Y, Z, le_out_aa(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
↳ PrologToPiTRSProof
U3_G(X, Y, Z, le_out_aa(X, Y)) → SORTED_IN_G(.(Y, Z))
SORTED_IN_G(.(X, .(Y, Z))) → U3_G(X, Y, Z, le_in_aa(X, Y))
le_in_aa(s(X), s(Y)) → U8_aa(X, Y, le_in_aa(X, Y))
le_in_aa(0, s(X)) → le_out_aa(0, s(X))
le_in_aa(0, 0) → le_out_aa(0, 0)
U8_aa(X, Y, le_out_aa(X, Y)) → le_out_aa(s(X), s(Y))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ PiDP
↳ PiDP
↳ PrologToPiTRSProof
SORTED_IN_G(.) → U3_G(le_in_aa)
U3_G(le_out_aa(X, Y)) → SORTED_IN_G(.)
le_in_aa → U8_aa(le_in_aa)
le_in_aa → le_out_aa(0, s)
le_in_aa → le_out_aa(0, 0)
U8_aa(le_out_aa(X, Y)) → le_out_aa(s, s)
le_in_aa
U8_aa(x0)
SORTED_IN_G(.) → U3_G(U8_aa(le_in_aa))
SORTED_IN_G(.) → U3_G(le_out_aa(0, s))
SORTED_IN_G(.) → U3_G(le_out_aa(0, 0))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ NonTerminationProof
↳ PiDP
↳ PiDP
↳ PrologToPiTRSProof
SORTED_IN_G(.) → U3_G(le_out_aa(0, s))
SORTED_IN_G(.) → U3_G(le_out_aa(0, 0))
U3_G(le_out_aa(X, Y)) → SORTED_IN_G(.)
SORTED_IN_G(.) → U3_G(U8_aa(le_in_aa))
le_in_aa → U8_aa(le_in_aa)
le_in_aa → le_out_aa(0, s)
le_in_aa → le_out_aa(0, 0)
U8_aa(le_out_aa(X, Y)) → le_out_aa(s, s)
le_in_aa
U8_aa(x0)
SORTED_IN_G(.) → U3_G(le_out_aa(0, s))
SORTED_IN_G(.) → U3_G(le_out_aa(0, 0))
U3_G(le_out_aa(X, Y)) → SORTED_IN_G(.)
SORTED_IN_G(.) → U3_G(U8_aa(le_in_aa))
le_in_aa → U8_aa(le_in_aa)
le_in_aa → le_out_aa(0, s)
le_in_aa → le_out_aa(0, 0)
U8_aa(le_out_aa(X, Y)) → le_out_aa(s, s)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PrologToPiTRSProof
DELETE_IN_AAA(X, .(Y, Z), W) → DELETE_IN_AAA(X, Z, W)
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(Y, Z), W) → U7_aga(X, Y, Z, W, delete_in_aaa(X, Z, W))
delete_in_aaa(X, .(X, Y), Y) → delete_out_aaa(X, .(X, Y), Y)
delete_in_aaa(X, .(Y, Z), W) → U7_aaa(X, Y, Z, W, delete_in_aaa(X, Z, W))
U7_aaa(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aaa(X, .(Y, Z), W)
U7_aga(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aga(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_aa(Z, V))
perm_in_aa([], []) → perm_out_aa([], [])
perm_in_aa(.(X, .(Y, [])), .(U, .(V, []))) → U5_aa(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
U5_aa(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_aa(X, Y, U, V, perm_in_aa(Z, V))
U6_aa(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_aa(.(X, .(Y, [])), .(U, .(V, [])))
U6_ag(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_aa(X, Y))
le_in_aa(s(X), s(Y)) → U8_aa(X, Y, le_in_aa(X, Y))
le_in_aa(0, s(X)) → le_out_aa(0, s(X))
le_in_aa(0, 0) → le_out_aa(0, 0)
U8_aa(X, Y, le_out_aa(X, Y)) → le_out_aa(s(X), s(Y))
U3_g(X, Y, Z, le_out_aa(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PrologToPiTRSProof
DELETE_IN_AAA(X, .(Y, Z), W) → DELETE_IN_AAA(X, Z, W)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ NonTerminationProof
↳ PiDP
↳ PrologToPiTRSProof
DELETE_IN_AAA → DELETE_IN_AAA
DELETE_IN_AAA → DELETE_IN_AAA
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PrologToPiTRSProof
PERM_IN_AA(.(X, .(Y, [])), .(U, .(V, []))) → U5_AA(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
U5_AA(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → PERM_IN_AA(Z, V)
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(Y, Z), W) → U7_aga(X, Y, Z, W, delete_in_aaa(X, Z, W))
delete_in_aaa(X, .(X, Y), Y) → delete_out_aaa(X, .(X, Y), Y)
delete_in_aaa(X, .(Y, Z), W) → U7_aaa(X, Y, Z, W, delete_in_aaa(X, Z, W))
U7_aaa(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aaa(X, .(Y, Z), W)
U7_aga(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aga(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_aa(Z, V))
perm_in_aa([], []) → perm_out_aa([], [])
perm_in_aa(.(X, .(Y, [])), .(U, .(V, []))) → U5_aa(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
U5_aa(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_aa(X, Y, U, V, perm_in_aa(Z, V))
U6_aa(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_aa(.(X, .(Y, [])), .(U, .(V, [])))
U6_ag(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_aa(X, Y))
le_in_aa(s(X), s(Y)) → U8_aa(X, Y, le_in_aa(X, Y))
le_in_aa(0, s(X)) → le_out_aa(0, s(X))
le_in_aa(0, 0) → le_out_aa(0, 0)
U8_aa(X, Y, le_out_aa(X, Y)) → le_out_aa(s(X), s(Y))
U3_g(X, Y, Z, le_out_aa(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PrologToPiTRSProof
PERM_IN_AA(.(X, .(Y, [])), .(U, .(V, []))) → U5_AA(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
U5_AA(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → PERM_IN_AA(Z, V)
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(Y, Z), W) → U7_aga(X, Y, Z, W, delete_in_aaa(X, Z, W))
U7_aga(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aga(X, .(Y, Z), W)
delete_in_aaa(X, .(X, Y), Y) → delete_out_aaa(X, .(X, Y), Y)
delete_in_aaa(X, .(Y, Z), W) → U7_aaa(X, Y, Z, W, delete_in_aaa(X, Z, W))
U7_aaa(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aaa(X, .(Y, Z), W)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ PrologToPiTRSProof
PERM_IN_AA → U5_AA(delete_in_aga(.))
U5_AA(delete_out_aga) → PERM_IN_AA
delete_in_aga(.) → delete_out_aga
delete_in_aga(.) → U7_aga(delete_in_aaa)
U7_aga(delete_out_aaa(Z)) → delete_out_aga
delete_in_aaa → delete_out_aaa(.)
delete_in_aaa → U7_aaa(delete_in_aaa)
U7_aaa(delete_out_aaa(Z)) → delete_out_aaa(.)
delete_in_aga(x0)
U7_aga(x0)
delete_in_aaa
U7_aaa(x0)
PERM_IN_AA → U5_AA(delete_out_aga)
PERM_IN_AA → U5_AA(U7_aga(delete_in_aaa))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ PrologToPiTRSProof
PERM_IN_AA → U5_AA(U7_aga(delete_in_aaa))
U5_AA(delete_out_aga) → PERM_IN_AA
PERM_IN_AA → U5_AA(delete_out_aga)
delete_in_aga(.) → delete_out_aga
delete_in_aga(.) → U7_aga(delete_in_aaa)
U7_aga(delete_out_aaa(Z)) → delete_out_aga
delete_in_aaa → delete_out_aaa(.)
delete_in_aaa → U7_aaa(delete_in_aaa)
U7_aaa(delete_out_aaa(Z)) → delete_out_aaa(.)
delete_in_aga(x0)
U7_aga(x0)
delete_in_aaa
U7_aaa(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ PrologToPiTRSProof
PERM_IN_AA → U5_AA(U7_aga(delete_in_aaa))
U5_AA(delete_out_aga) → PERM_IN_AA
PERM_IN_AA → U5_AA(delete_out_aga)
delete_in_aaa → delete_out_aaa(.)
delete_in_aaa → U7_aaa(delete_in_aaa)
U7_aga(delete_out_aaa(Z)) → delete_out_aga
U7_aaa(delete_out_aaa(Z)) → delete_out_aaa(.)
delete_in_aga(x0)
U7_aga(x0)
delete_in_aaa
U7_aaa(x0)
delete_in_aga(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ NonTerminationProof
↳ PrologToPiTRSProof
PERM_IN_AA → U5_AA(U7_aga(delete_in_aaa))
U5_AA(delete_out_aga) → PERM_IN_AA
PERM_IN_AA → U5_AA(delete_out_aga)
delete_in_aaa → delete_out_aaa(.)
delete_in_aaa → U7_aaa(delete_in_aaa)
U7_aga(delete_out_aaa(Z)) → delete_out_aga
U7_aaa(delete_out_aaa(Z)) → delete_out_aaa(.)
U7_aga(x0)
delete_in_aaa
U7_aaa(x0)
PERM_IN_AA → U5_AA(U7_aga(delete_in_aaa))
U5_AA(delete_out_aga) → PERM_IN_AA
PERM_IN_AA → U5_AA(delete_out_aga)
delete_in_aaa → delete_out_aaa(.)
delete_in_aaa → U7_aaa(delete_in_aaa)
U7_aga(delete_out_aaa(Z)) → delete_out_aga
U7_aaa(delete_out_aaa(Z)) → delete_out_aaa(.)
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(Y, Z), W) → U7_aga(X, Y, Z, W, delete_in_aaa(X, Z, W))
delete_in_aaa(X, .(X, Y), Y) → delete_out_aaa(X, .(X, Y), Y)
delete_in_aaa(X, .(Y, Z), W) → U7_aaa(X, Y, Z, W, delete_in_aaa(X, Z, W))
U7_aaa(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aaa(X, .(Y, Z), W)
U7_aga(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aga(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_aa(Z, V))
perm_in_aa([], []) → perm_out_aa([], [])
perm_in_aa(.(X, .(Y, [])), .(U, .(V, []))) → U5_aa(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
U5_aa(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_aa(X, Y, U, V, perm_in_aa(Z, V))
U6_aa(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_aa(.(X, .(Y, [])), .(U, .(V, [])))
U6_ag(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_aa(X, Y))
le_in_aa(s(X), s(Y)) → U8_aa(X, Y, le_in_aa(X, Y))
le_in_aa(0, s(X)) → le_out_aa(0, s(X))
le_in_aa(0, 0) → le_out_aa(0, 0)
U8_aa(X, Y, le_out_aa(X, Y)) → le_out_aa(s(X), s(Y))
U3_g(X, Y, Z, le_out_aa(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(Y, Z), W) → U7_aga(X, Y, Z, W, delete_in_aaa(X, Z, W))
delete_in_aaa(X, .(X, Y), Y) → delete_out_aaa(X, .(X, Y), Y)
delete_in_aaa(X, .(Y, Z), W) → U7_aaa(X, Y, Z, W, delete_in_aaa(X, Z, W))
U7_aaa(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aaa(X, .(Y, Z), W)
U7_aga(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aga(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_aa(Z, V))
perm_in_aa([], []) → perm_out_aa([], [])
perm_in_aa(.(X, .(Y, [])), .(U, .(V, []))) → U5_aa(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
U5_aa(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_aa(X, Y, U, V, perm_in_aa(Z, V))
U6_aa(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_aa(.(X, .(Y, [])), .(U, .(V, [])))
U6_ag(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_aa(X, Y))
le_in_aa(s(X), s(Y)) → U8_aa(X, Y, le_in_aa(X, Y))
le_in_aa(0, s(X)) → le_out_aa(0, s(X))
le_in_aa(0, 0) → le_out_aa(0, 0)
U8_aa(X, Y, le_out_aa(X, Y)) → le_out_aa(s(X), s(Y))
U3_g(X, Y, Z, le_out_aa(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
SLOWSORT_IN_AG(X, Y) → U1_AG(X, Y, perm_in_ag(X, Y))
SLOWSORT_IN_AG(X, Y) → PERM_IN_AG(X, Y)
PERM_IN_AG(.(X, .(Y, [])), .(U, .(V, []))) → U5_AG(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
PERM_IN_AG(.(X, .(Y, [])), .(U, .(V, []))) → DELETE_IN_AGA(U, .(X, Y), Z)
DELETE_IN_AGA(X, .(Y, Z), W) → U7_AGA(X, Y, Z, W, delete_in_aaa(X, Z, W))
DELETE_IN_AGA(X, .(Y, Z), W) → DELETE_IN_AAA(X, Z, W)
DELETE_IN_AAA(X, .(Y, Z), W) → U7_AAA(X, Y, Z, W, delete_in_aaa(X, Z, W))
DELETE_IN_AAA(X, .(Y, Z), W) → DELETE_IN_AAA(X, Z, W)
U5_AG(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_AG(X, Y, U, V, perm_in_aa(Z, V))
U5_AG(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → PERM_IN_AA(Z, V)
PERM_IN_AA(.(X, .(Y, [])), .(U, .(V, []))) → U5_AA(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
PERM_IN_AA(.(X, .(Y, [])), .(U, .(V, []))) → DELETE_IN_AGA(U, .(X, Y), Z)
U5_AA(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_AA(X, Y, U, V, perm_in_aa(Z, V))
U5_AA(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → PERM_IN_AA(Z, V)
U1_AG(X, Y, perm_out_ag(X, Y)) → U2_AG(X, Y, sorted_in_g(Y))
U1_AG(X, Y, perm_out_ag(X, Y)) → SORTED_IN_G(Y)
SORTED_IN_G(.(X, .(Y, Z))) → U3_G(X, Y, Z, le_in_aa(X, Y))
SORTED_IN_G(.(X, .(Y, Z))) → LE_IN_AA(X, Y)
LE_IN_AA(s(X), s(Y)) → U8_AA(X, Y, le_in_aa(X, Y))
LE_IN_AA(s(X), s(Y)) → LE_IN_AA(X, Y)
U3_G(X, Y, Z, le_out_aa(X, Y)) → U4_G(X, Y, Z, sorted_in_g(.(Y, Z)))
U3_G(X, Y, Z, le_out_aa(X, Y)) → SORTED_IN_G(.(Y, Z))
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(Y, Z), W) → U7_aga(X, Y, Z, W, delete_in_aaa(X, Z, W))
delete_in_aaa(X, .(X, Y), Y) → delete_out_aaa(X, .(X, Y), Y)
delete_in_aaa(X, .(Y, Z), W) → U7_aaa(X, Y, Z, W, delete_in_aaa(X, Z, W))
U7_aaa(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aaa(X, .(Y, Z), W)
U7_aga(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aga(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_aa(Z, V))
perm_in_aa([], []) → perm_out_aa([], [])
perm_in_aa(.(X, .(Y, [])), .(U, .(V, []))) → U5_aa(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
U5_aa(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_aa(X, Y, U, V, perm_in_aa(Z, V))
U6_aa(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_aa(.(X, .(Y, [])), .(U, .(V, [])))
U6_ag(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_aa(X, Y))
le_in_aa(s(X), s(Y)) → U8_aa(X, Y, le_in_aa(X, Y))
le_in_aa(0, s(X)) → le_out_aa(0, s(X))
le_in_aa(0, 0) → le_out_aa(0, 0)
U8_aa(X, Y, le_out_aa(X, Y)) → le_out_aa(s(X), s(Y))
U3_g(X, Y, Z, le_out_aa(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
SLOWSORT_IN_AG(X, Y) → U1_AG(X, Y, perm_in_ag(X, Y))
SLOWSORT_IN_AG(X, Y) → PERM_IN_AG(X, Y)
PERM_IN_AG(.(X, .(Y, [])), .(U, .(V, []))) → U5_AG(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
PERM_IN_AG(.(X, .(Y, [])), .(U, .(V, []))) → DELETE_IN_AGA(U, .(X, Y), Z)
DELETE_IN_AGA(X, .(Y, Z), W) → U7_AGA(X, Y, Z, W, delete_in_aaa(X, Z, W))
DELETE_IN_AGA(X, .(Y, Z), W) → DELETE_IN_AAA(X, Z, W)
DELETE_IN_AAA(X, .(Y, Z), W) → U7_AAA(X, Y, Z, W, delete_in_aaa(X, Z, W))
DELETE_IN_AAA(X, .(Y, Z), W) → DELETE_IN_AAA(X, Z, W)
U5_AG(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_AG(X, Y, U, V, perm_in_aa(Z, V))
U5_AG(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → PERM_IN_AA(Z, V)
PERM_IN_AA(.(X, .(Y, [])), .(U, .(V, []))) → U5_AA(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
PERM_IN_AA(.(X, .(Y, [])), .(U, .(V, []))) → DELETE_IN_AGA(U, .(X, Y), Z)
U5_AA(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_AA(X, Y, U, V, perm_in_aa(Z, V))
U5_AA(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → PERM_IN_AA(Z, V)
U1_AG(X, Y, perm_out_ag(X, Y)) → U2_AG(X, Y, sorted_in_g(Y))
U1_AG(X, Y, perm_out_ag(X, Y)) → SORTED_IN_G(Y)
SORTED_IN_G(.(X, .(Y, Z))) → U3_G(X, Y, Z, le_in_aa(X, Y))
SORTED_IN_G(.(X, .(Y, Z))) → LE_IN_AA(X, Y)
LE_IN_AA(s(X), s(Y)) → U8_AA(X, Y, le_in_aa(X, Y))
LE_IN_AA(s(X), s(Y)) → LE_IN_AA(X, Y)
U3_G(X, Y, Z, le_out_aa(X, Y)) → U4_G(X, Y, Z, sorted_in_g(.(Y, Z)))
U3_G(X, Y, Z, le_out_aa(X, Y)) → SORTED_IN_G(.(Y, Z))
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(Y, Z), W) → U7_aga(X, Y, Z, W, delete_in_aaa(X, Z, W))
delete_in_aaa(X, .(X, Y), Y) → delete_out_aaa(X, .(X, Y), Y)
delete_in_aaa(X, .(Y, Z), W) → U7_aaa(X, Y, Z, W, delete_in_aaa(X, Z, W))
U7_aaa(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aaa(X, .(Y, Z), W)
U7_aga(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aga(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_aa(Z, V))
perm_in_aa([], []) → perm_out_aa([], [])
perm_in_aa(.(X, .(Y, [])), .(U, .(V, []))) → U5_aa(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
U5_aa(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_aa(X, Y, U, V, perm_in_aa(Z, V))
U6_aa(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_aa(.(X, .(Y, [])), .(U, .(V, [])))
U6_ag(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_aa(X, Y))
le_in_aa(s(X), s(Y)) → U8_aa(X, Y, le_in_aa(X, Y))
le_in_aa(0, s(X)) → le_out_aa(0, s(X))
le_in_aa(0, 0) → le_out_aa(0, 0)
U8_aa(X, Y, le_out_aa(X, Y)) → le_out_aa(s(X), s(Y))
U3_g(X, Y, Z, le_out_aa(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
↳ PiDP
LE_IN_AA(s(X), s(Y)) → LE_IN_AA(X, Y)
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(Y, Z), W) → U7_aga(X, Y, Z, W, delete_in_aaa(X, Z, W))
delete_in_aaa(X, .(X, Y), Y) → delete_out_aaa(X, .(X, Y), Y)
delete_in_aaa(X, .(Y, Z), W) → U7_aaa(X, Y, Z, W, delete_in_aaa(X, Z, W))
U7_aaa(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aaa(X, .(Y, Z), W)
U7_aga(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aga(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_aa(Z, V))
perm_in_aa([], []) → perm_out_aa([], [])
perm_in_aa(.(X, .(Y, [])), .(U, .(V, []))) → U5_aa(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
U5_aa(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_aa(X, Y, U, V, perm_in_aa(Z, V))
U6_aa(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_aa(.(X, .(Y, [])), .(U, .(V, [])))
U6_ag(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_aa(X, Y))
le_in_aa(s(X), s(Y)) → U8_aa(X, Y, le_in_aa(X, Y))
le_in_aa(0, s(X)) → le_out_aa(0, s(X))
le_in_aa(0, 0) → le_out_aa(0, 0)
U8_aa(X, Y, le_out_aa(X, Y)) → le_out_aa(s(X), s(Y))
U3_g(X, Y, Z, le_out_aa(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
↳ PiDP
LE_IN_AA(s(X), s(Y)) → LE_IN_AA(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ NonTerminationProof
↳ PiDP
↳ PiDP
↳ PiDP
LE_IN_AA → LE_IN_AA
LE_IN_AA → LE_IN_AA
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
U3_G(X, Y, Z, le_out_aa(X, Y)) → SORTED_IN_G(.(Y, Z))
SORTED_IN_G(.(X, .(Y, Z))) → U3_G(X, Y, Z, le_in_aa(X, Y))
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(Y, Z), W) → U7_aga(X, Y, Z, W, delete_in_aaa(X, Z, W))
delete_in_aaa(X, .(X, Y), Y) → delete_out_aaa(X, .(X, Y), Y)
delete_in_aaa(X, .(Y, Z), W) → U7_aaa(X, Y, Z, W, delete_in_aaa(X, Z, W))
U7_aaa(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aaa(X, .(Y, Z), W)
U7_aga(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aga(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_aa(Z, V))
perm_in_aa([], []) → perm_out_aa([], [])
perm_in_aa(.(X, .(Y, [])), .(U, .(V, []))) → U5_aa(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
U5_aa(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_aa(X, Y, U, V, perm_in_aa(Z, V))
U6_aa(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_aa(.(X, .(Y, [])), .(U, .(V, [])))
U6_ag(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_aa(X, Y))
le_in_aa(s(X), s(Y)) → U8_aa(X, Y, le_in_aa(X, Y))
le_in_aa(0, s(X)) → le_out_aa(0, s(X))
le_in_aa(0, 0) → le_out_aa(0, 0)
U8_aa(X, Y, le_out_aa(X, Y)) → le_out_aa(s(X), s(Y))
U3_g(X, Y, Z, le_out_aa(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
U3_G(X, Y, Z, le_out_aa(X, Y)) → SORTED_IN_G(.(Y, Z))
SORTED_IN_G(.(X, .(Y, Z))) → U3_G(X, Y, Z, le_in_aa(X, Y))
le_in_aa(s(X), s(Y)) → U8_aa(X, Y, le_in_aa(X, Y))
le_in_aa(0, s(X)) → le_out_aa(0, s(X))
le_in_aa(0, 0) → le_out_aa(0, 0)
U8_aa(X, Y, le_out_aa(X, Y)) → le_out_aa(s(X), s(Y))
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ PiDP
↳ PiDP
SORTED_IN_G(.) → U3_G(le_in_aa)
U3_G(le_out_aa(X, Y)) → SORTED_IN_G(.)
le_in_aa → U8_aa(le_in_aa)
le_in_aa → le_out_aa(0, s)
le_in_aa → le_out_aa(0, 0)
U8_aa(le_out_aa(X, Y)) → le_out_aa(s, s)
le_in_aa
U8_aa(x0)
SORTED_IN_G(.) → U3_G(U8_aa(le_in_aa))
SORTED_IN_G(.) → U3_G(le_out_aa(0, s))
SORTED_IN_G(.) → U3_G(le_out_aa(0, 0))
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ NonTerminationProof
↳ PiDP
↳ PiDP
SORTED_IN_G(.) → U3_G(le_out_aa(0, s))
SORTED_IN_G(.) → U3_G(le_out_aa(0, 0))
U3_G(le_out_aa(X, Y)) → SORTED_IN_G(.)
SORTED_IN_G(.) → U3_G(U8_aa(le_in_aa))
le_in_aa → U8_aa(le_in_aa)
le_in_aa → le_out_aa(0, s)
le_in_aa → le_out_aa(0, 0)
U8_aa(le_out_aa(X, Y)) → le_out_aa(s, s)
le_in_aa
U8_aa(x0)
SORTED_IN_G(.) → U3_G(le_out_aa(0, s))
SORTED_IN_G(.) → U3_G(le_out_aa(0, 0))
U3_G(le_out_aa(X, Y)) → SORTED_IN_G(.)
SORTED_IN_G(.) → U3_G(U8_aa(le_in_aa))
le_in_aa → U8_aa(le_in_aa)
le_in_aa → le_out_aa(0, s)
le_in_aa → le_out_aa(0, 0)
U8_aa(le_out_aa(X, Y)) → le_out_aa(s, s)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
DELETE_IN_AAA(X, .(Y, Z), W) → DELETE_IN_AAA(X, Z, W)
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(Y, Z), W) → U7_aga(X, Y, Z, W, delete_in_aaa(X, Z, W))
delete_in_aaa(X, .(X, Y), Y) → delete_out_aaa(X, .(X, Y), Y)
delete_in_aaa(X, .(Y, Z), W) → U7_aaa(X, Y, Z, W, delete_in_aaa(X, Z, W))
U7_aaa(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aaa(X, .(Y, Z), W)
U7_aga(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aga(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_aa(Z, V))
perm_in_aa([], []) → perm_out_aa([], [])
perm_in_aa(.(X, .(Y, [])), .(U, .(V, []))) → U5_aa(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
U5_aa(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_aa(X, Y, U, V, perm_in_aa(Z, V))
U6_aa(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_aa(.(X, .(Y, [])), .(U, .(V, [])))
U6_ag(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_aa(X, Y))
le_in_aa(s(X), s(Y)) → U8_aa(X, Y, le_in_aa(X, Y))
le_in_aa(0, s(X)) → le_out_aa(0, s(X))
le_in_aa(0, 0) → le_out_aa(0, 0)
U8_aa(X, Y, le_out_aa(X, Y)) → le_out_aa(s(X), s(Y))
U3_g(X, Y, Z, le_out_aa(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
DELETE_IN_AAA(X, .(Y, Z), W) → DELETE_IN_AAA(X, Z, W)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ NonTerminationProof
↳ PiDP
DELETE_IN_AAA → DELETE_IN_AAA
DELETE_IN_AAA → DELETE_IN_AAA
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
PERM_IN_AA(.(X, .(Y, [])), .(U, .(V, []))) → U5_AA(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
U5_AA(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → PERM_IN_AA(Z, V)
slowsort_in_ag(X, Y) → U1_ag(X, Y, perm_in_ag(X, Y))
perm_in_ag([], []) → perm_out_ag([], [])
perm_in_ag(.(X, .(Y, [])), .(U, .(V, []))) → U5_ag(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(Y, Z), W) → U7_aga(X, Y, Z, W, delete_in_aaa(X, Z, W))
delete_in_aaa(X, .(X, Y), Y) → delete_out_aaa(X, .(X, Y), Y)
delete_in_aaa(X, .(Y, Z), W) → U7_aaa(X, Y, Z, W, delete_in_aaa(X, Z, W))
U7_aaa(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aaa(X, .(Y, Z), W)
U7_aga(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aga(X, .(Y, Z), W)
U5_ag(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_ag(X, Y, U, V, perm_in_aa(Z, V))
perm_in_aa([], []) → perm_out_aa([], [])
perm_in_aa(.(X, .(Y, [])), .(U, .(V, []))) → U5_aa(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
U5_aa(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → U6_aa(X, Y, U, V, perm_in_aa(Z, V))
U6_aa(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_aa(.(X, .(Y, [])), .(U, .(V, [])))
U6_ag(X, Y, U, V, perm_out_aa(Z, V)) → perm_out_ag(.(X, .(Y, [])), .(U, .(V, [])))
U1_ag(X, Y, perm_out_ag(X, Y)) → U2_ag(X, Y, sorted_in_g(Y))
sorted_in_g([]) → sorted_out_g([])
sorted_in_g(.(X, [])) → sorted_out_g(.(X, []))
sorted_in_g(.(X, .(Y, Z))) → U3_g(X, Y, Z, le_in_aa(X, Y))
le_in_aa(s(X), s(Y)) → U8_aa(X, Y, le_in_aa(X, Y))
le_in_aa(0, s(X)) → le_out_aa(0, s(X))
le_in_aa(0, 0) → le_out_aa(0, 0)
U8_aa(X, Y, le_out_aa(X, Y)) → le_out_aa(s(X), s(Y))
U3_g(X, Y, Z, le_out_aa(X, Y)) → U4_g(X, Y, Z, sorted_in_g(.(Y, Z)))
U4_g(X, Y, Z, sorted_out_g(.(Y, Z))) → sorted_out_g(.(X, .(Y, Z)))
U2_ag(X, Y, sorted_out_g(Y)) → slowsort_out_ag(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
PERM_IN_AA(.(X, .(Y, [])), .(U, .(V, []))) → U5_AA(X, Y, U, V, delete_in_aga(U, .(X, Y), Z))
U5_AA(X, Y, U, V, delete_out_aga(U, .(X, Y), Z)) → PERM_IN_AA(Z, V)
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(Y, Z), W) → U7_aga(X, Y, Z, W, delete_in_aaa(X, Z, W))
U7_aga(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aga(X, .(Y, Z), W)
delete_in_aaa(X, .(X, Y), Y) → delete_out_aaa(X, .(X, Y), Y)
delete_in_aaa(X, .(Y, Z), W) → U7_aaa(X, Y, Z, W, delete_in_aaa(X, Z, W))
U7_aaa(X, Y, Z, W, delete_out_aaa(X, Z, W)) → delete_out_aaa(X, .(Y, Z), W)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
U5_AA(delete_out_aga(.)) → PERM_IN_AA
PERM_IN_AA → U5_AA(delete_in_aga(.))
delete_in_aga(.) → delete_out_aga(.)
delete_in_aga(.) → U7_aga(delete_in_aaa)
U7_aga(delete_out_aaa(Z)) → delete_out_aga(.)
delete_in_aaa → delete_out_aaa(.)
delete_in_aaa → U7_aaa(delete_in_aaa)
U7_aaa(delete_out_aaa(Z)) → delete_out_aaa(.)
delete_in_aga(x0)
U7_aga(x0)
delete_in_aaa
U7_aaa(x0)
PERM_IN_AA → U5_AA(delete_out_aga(.))
PERM_IN_AA → U5_AA(U7_aga(delete_in_aaa))
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
U5_AA(delete_out_aga(.)) → PERM_IN_AA
PERM_IN_AA → U5_AA(U7_aga(delete_in_aaa))
PERM_IN_AA → U5_AA(delete_out_aga(.))
delete_in_aga(.) → delete_out_aga(.)
delete_in_aga(.) → U7_aga(delete_in_aaa)
U7_aga(delete_out_aaa(Z)) → delete_out_aga(.)
delete_in_aaa → delete_out_aaa(.)
delete_in_aaa → U7_aaa(delete_in_aaa)
U7_aaa(delete_out_aaa(Z)) → delete_out_aaa(.)
delete_in_aga(x0)
U7_aga(x0)
delete_in_aaa
U7_aaa(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
U5_AA(delete_out_aga(.)) → PERM_IN_AA
PERM_IN_AA → U5_AA(U7_aga(delete_in_aaa))
PERM_IN_AA → U5_AA(delete_out_aga(.))
delete_in_aaa → delete_out_aaa(.)
delete_in_aaa → U7_aaa(delete_in_aaa)
U7_aga(delete_out_aaa(Z)) → delete_out_aga(.)
U7_aaa(delete_out_aaa(Z)) → delete_out_aaa(.)
delete_in_aga(x0)
U7_aga(x0)
delete_in_aaa
U7_aaa(x0)
delete_in_aga(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ NonTerminationProof
U5_AA(delete_out_aga(.)) → PERM_IN_AA
PERM_IN_AA → U5_AA(U7_aga(delete_in_aaa))
PERM_IN_AA → U5_AA(delete_out_aga(.))
delete_in_aaa → delete_out_aaa(.)
delete_in_aaa → U7_aaa(delete_in_aaa)
U7_aga(delete_out_aaa(Z)) → delete_out_aga(.)
U7_aaa(delete_out_aaa(Z)) → delete_out_aaa(.)
U7_aga(x0)
delete_in_aaa
U7_aaa(x0)
U5_AA(delete_out_aga(.)) → PERM_IN_AA
PERM_IN_AA → U5_AA(U7_aga(delete_in_aaa))
PERM_IN_AA → U5_AA(delete_out_aga(.))
delete_in_aaa → delete_out_aaa(.)
delete_in_aaa → U7_aaa(delete_in_aaa)
U7_aga(delete_out_aaa(Z)) → delete_out_aga(.)
U7_aaa(delete_out_aaa(Z)) → delete_out_aaa(.)